(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Int)
(declare-fun x_1 () (Array Int Int))
(declare-fun x_2 () Int)
(declare-fun x_3 () (Array Int Int))
(declare-fun x_4 () Int)
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () Int)
(declare-fun x_11 () (Array Int Int))
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () (Array Int Int))
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () (Array Int Int))
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () (Array Int Int))
(declare-fun x_24 () Int)
(declare-fun x_25 () Int)
(declare-fun x_26 () Int)
(declare-fun x_27 () (Array Int Int))
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () (Array Int Int))
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () (Array Int Int))
(declare-fun x_35 () (Array Int Int))
(declare-fun x_36 () (Array Int Int))
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () (Array Int Int))
(assert (let ((?v_16 (= x_2 0)) (?v_10 (= x_12 1)) (?v_2 (not (<= x_26 0))) (?v_11 (not (<= x_14 0))) (?v_1 (= x_24 1)) (?v_20 (= x_24 0)) (?v_4 (= x_20 1)) (?v_8 (not (<= x_18 0))) (?v_24 (= x_5 0)) (?v_25 (= x_0 0)) (?v_19 (= x_28 0)) (?v_5 (not (<= x_22 0))) (?v_15 (= x_5 1)) (?v_23 (= x_12 0)) (?v_17 (not (<= x_10 0))) (?v_0 (= x_28 1)) (?v_7 (= x_16 1)) (?v_22 (= x_16 0)) (?v_21 (= x_20 0)) (?v_13 (not (<= x_0 0))) (?v_14 (- x_0 1)) (?v_3 (- x_26 1)) (?v_6 (- x_22 1)) (?v_9 (- x_18 1)) (?v_12 (- x_14 1)) (?v_18 (- x_10 1))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_32 2) (>= x_32 0)) (<= x_28 2)) (>= x_28 0)) (<= x_24 2)) (>= x_24 0)) (<= x_20 2)) (>= x_20 0)) (<= x_16 2)) (>= x_16 0)) (<= x_12 2)) (>= x_12 0)) (<= x_5 2)) (>= x_5 0)) (not (< x_0 0))) (not (< x_2 0))) (not (< x_10 0))) (not (< x_13 0))) (not (< x_14 0))) (not (< x_17 0))) (not (< x_18 0))) (not (< x_21 0))) (not (< x_22 0))) (not (< x_25 0))) (not (< x_26 0))) (not (< x_29 0))) (not (< x_30 0))) (not (< x_33 0))) ?v_25) ?v_16) (= x_32 (ite (<= x_33 2) 1 (ite (<= x_33 5) 0 2)))) (= x_28 (ite (<= x_29 2) 1 (ite (<= x_29 5) 0 2)))) (= x_24 (ite (<= x_25 2) 1 (ite (<= x_25 5) 0 2)))) (= x_20 (ite (<= x_21 2) 1 (ite (<= x_21 5) 0 2)))) (= x_16 (ite (<= x_17 2) 1 (ite (<= x_17 5) 0 2)))) (= x_12 (ite (<= x_13 2) 1 (ite (<= x_13 5) 0 2)))) (= (select x_3 0) (ite ?v_13 (select x_1 ?v_14) x_4))) (= x_5 (ite (<= x_2 2) 1 (ite (<= x_2 5) 0 2)))) (= x_30 (ite ?v_0 (+ x_26 1) (ite (and ?v_19 ?v_2) ?v_3 x_26)))) (= x_31 (ite ?v_0 (store x_27 x_26 (ite (= x_29 0) x_6 (ite (= x_29 1) x_7 (ite (= x_29 2) x_8 x_9)))) x_27))) (= x_33 (+ x_29 1))) (= x_26 (ite ?v_1 (+ x_22 1) (ite (and ?v_20 ?v_5) ?v_6 x_22)))) (= x_27 (ite ?v_1 (store x_23 x_22 (ite (= x_25 0) x_6 (ite (= x_25 1) x_7 (ite (= x_25 2) x_8 x_9)))) x_23))) (= x_29 (+ x_25 1))) (= x_38 (store x_37 x_29 (ite ?v_2 (select x_27 ?v_3) x_4)))) (= x_22 (ite ?v_4 (+ x_18 1) (ite (and ?v_21 ?v_8) ?v_9 x_18)))) (= x_23 (ite ?v_4 (store x_19 x_18 (ite (= x_21 0) x_6 (ite (= x_21 1) x_7 (ite (= x_21 2) x_8 x_9)))) x_19))) (= x_25 (+ x_21 1))) (= x_37 (store x_36 x_25 (ite ?v_5 (select x_23 ?v_6) x_4)))) (= x_18 (ite ?v_7 (+ x_14 1) (ite (and ?v_22 ?v_11) ?v_12 x_14)))) (= x_19 (ite ?v_7 (store x_15 x_14 (ite (= x_17 0) x_6 (ite (= x_17 1) x_7 (ite (= x_17 2) x_8 x_9)))) x_15))) (= x_21 (+ x_17 1))) (= x_36 (store x_35 x_21 (ite ?v_8 (select x_19 ?v_9) x_4)))) (= x_14 (ite ?v_10 (+ x_10 1) (ite (and ?v_23 ?v_17) ?v_18 x_10)))) (= x_15 (ite ?v_10 (store x_11 x_10 (ite (= x_13 0) x_6 (ite (= x_13 1) x_7 (ite (= x_13 2) x_8 x_9)))) x_11))) (= x_17 (+ x_13 1))) (= x_35 (store x_34 x_17 (ite ?v_11 (select x_15 ?v_12) x_4)))) (= x_10 (ite ?v_15 (+ x_0 1) (ite (and ?v_24 ?v_13) ?v_14 x_0)))) (= x_11 (ite ?v_15 (store x_1 x_0 (ite ?v_16 x_6 (ite (= x_2 1) x_7 (ite (= x_2 2) x_8 x_9)))) x_1))) (= x_13 (+ x_2 1))) (= x_34 (store x_3 x_13 (ite ?v_17 (select x_11 ?v_18) x_4)))) (or (or (or (or (or (or (and (= x_32 0) (= x_30 0)) (and ?v_19 (= x_26 0))) (and ?v_20 (= x_22 0))) (and ?v_21 (= x_18 0))) (and ?v_22 (= x_14 0))) (and ?v_23 (= x_10 0))) (and ?v_24 ?v_25)))))
(check-sat)
(exit)
